package fsmCore;


import interfaccia.Input;

import java.util.Vector;

import javax.swing.JOptionPane;


public class Simulazione {
	/*@
	  @ invariant \forall int i;_fsm[i]; i<NUMERO_MACCHINE && fsm[i]!=null;
	  @ invariant \forall int i;_fsm[i]; i<NUMERO_MACCHINE && fsm[i].getStatoIniziale()!=null
	  @*/
	
	private static final int NUMERO_MACCHINE=2;
	
	public static final int TUTTE_LE_TRANSIZIONI=1;
	public static final int SOLO_ASINCRONE=0;
	
	private Macchina fsm[];
	private int istanteCorrente;
	private Vector<Transizione> transAttive[];//usato come cache
	private Transizione transEffettuata[];//usato come cache
	private Transizione transInAtto[];//usato come cache


	

	
	public Simulazione(Macchina [] _fsm){
		fsm=_fsm;
		istanteCorrente=0;
		transAttive = new Vector[NUMERO_MACCHINE];//usato come cache
		transEffettuata = new Transizione[NUMERO_MACCHINE];//usato come cache
		transInAtto = new Transizione[NUMERO_MACCHINE];//usato come cache
	}
	
		/*test eseguiti con successo
		 * 
		 * sistema in deadlock
		 * stato finale
		 * 
		 * macchina 1	macchina 2
		 * sincrona		nessuna
		 * sincrona		sincrona non reciproc
		 * sincrona		reciprocamente sincrona
		 * asincrona	sincrona
		 * asincrona	asincrona
		 * 
		 * esegui con coppie di transizioni
		 */

	public void eseguiIterazione(){
		Transizione [] daEseguire= new Transizione[NUMERO_MACCHINE];
		
		
		daEseguire=getTransizioniDaEseguire();
	
		
		int durata =getDurataIterazione(daEseguire);//set della durata
		setIstanteCorrente(istanteCorrente+durata);
		
		for(int i=0; i<NUMERO_MACCHINE;i++){
			if(daEseguire[i]!=null){
				eseguiTransizione(daEseguire[i], i, durata);
							
			}
			else
				transEffettuata[i]=null;
		}
		
	
	}
	
	public boolean sistemaBloccato(){
		//il sistema è bloccato quando uno stato non ha transizioni attive
		if(transInAtto[0]==null&&transInAtto[1]==null&&getTransizioniAbilitate(0, TUTTE_LE_TRANSIZIONI).isEmpty()&&getTransizioniAbilitate(1, TUTTE_LE_TRANSIZIONI).isEmpty())
			return true;
		
		else
			return false;		
		
	}
	
	public boolean deadlock(){//non funziona
		if(fsm[0].getStatoCorrente().isFinale()&&fsm[1].getStatoCorrente().isFinale())
			return false;
		else
			return true;
		
	}
	
	public void impostaStatiIniziali(){
		for(int i=0;i<NUMERO_MACCHINE;i++){
			fsm[i].setStatoCorrente(fsm[i].getStatoIniziale());
			transInAtto[i]=null;
		}
	}
	
	/*
	 * questo metodo modifica il valore di trans attive
	 */
	/*@requires numerofsm<=NUMERO_MACCHINE
	  @			 
	  @
	  @ensure \result !=null &&
	  @ if(\exist "transizioni abilitate a scattare del tipo scelto") \result.size()>0
	  @       else\result.size()==0
	  @*/
	//Nota che una transizione in atto non è abilitata a scattare
	//type = 0 solo transizioni asincrone
	
	/*test eseguiti con successo
	 * ripeti x ogni type
	 * 
	 * no trans attive 
	 * attive sincrone non reciprocamente + asincrone
	 * attive sincrone reciprocamente + asincrone
	 * */
	private Vector<Transizione> getTransizioniAbilitate(int numeroFsm,int type){
		Vector<Transizione> abilitate=new Vector<Transizione>();
		
		setTransAttive();
				
		//verifica che non ci siano transizioni in atto
		Transizione t1,t2;
		for(int i=0; i<transAttive[numeroFsm].size(); i++){
			t1= transAttive[numeroFsm].get(i);
			
			if(t1.isInAtto())
				return abilitate;//trovando una transizione in atto si esce dal metodo restituendo un vettore vuoto
		}
		
		
		for(int i=0; i<transAttive[numeroFsm].size(); i++){
			t1= transAttive[numeroFsm].get(i);
			if(t1.getClass()==TransizioneAsincrona.class)//una transizione asincrona viene subito aggiunta alle transizioni abilitate 
				abilitate.add(t1);
			
			else if(type!=SOLO_ASINCRONE){//eseguito necessariamente quando la transizione t1 è sincrona e si vogliono trovare anche transizioni sincrone abilitate
				boolean trovato=false;
				for(int j=0; j<transAttive[(numeroFsm+1)%NUMERO_MACCHINE].size(); j++){//una transizione sincrona è aggiunta all transizioni abilitate solo se esiste una trans reciprocamente sincrona
					t2=transAttive[(numeroFsm+1)%NUMERO_MACCHINE].get(j);
					if(t2.getClass()==TransizioneSincrona.class)
						if(!trovato&&((TransizioneSincrona)t1).getClasseEq().equals(((TransizioneSincrona)t2).getClasseEq())){//verifica l'appartenenza alla stessa classe di equivalenza
							abilitate.add(t1);
							trovato=true;
		 			}
				}//for
			}//else
		}//for
			
		return abilitate;
		
	}

	
	/*@requires transAbilitate !=null
	  @
	  @ensure int numeroMAcchina;if (Deadlock(numeroMAcchina))\result[i]== null
	  @*/
	
	/*test da eseguire
	 * presenti abilitate coppia di sincrone + asincrone
	 * solo sincrone 
	 * solo asincrone
	 * una asincrona e null
	 * piu sincrone nella seconda
	 * solo una coppia di asincrone
	 * piu asincrone nella seconda
	 * coppia di null
	 * */
	private Transizione[] getTransizioniDaEseguire() {
		Transizione [] risultato=new Transizione[NUMERO_MACCHINE];
		
		/*viene impostato il valore della transizione da eseguire sulla macchina 1; null se nessuna transizione
		 * */
		Vector <Transizione> abilitate_1= getTransizioniAbilitate(0, TUTTE_LE_TRANSIZIONI);
		if(abilitate_1.size()==1)
			risultato[0]=abilitate_1.get(0);
		
		else if(abilitate_1.size()>1)
			risultato[0]=Input.selezionaTransizione("Seleziona la transizione da eseguire sulla macchina 1",abilitate_1);
		
		
		/*viene impostato il valore della transizione da eseguire sulla macchina 2; null se nessuna transizione
		 */
		if(risultato[0]!=null&&risultato[0].getClass()==TransizioneSincrona.class)
		{
			Vector <Transizione> reciprocamenteSincrone= getReciprocamenteSincrone((TransizioneSincrona)risultato[0], 1); //cerco le transizioni reciprocamente sincrone in fsm 2
						
			if(reciprocamenteSincrone.size()==1)
				risultato[1]=reciprocamenteSincrone.get(0);
			else
				risultato[1]=Input.selezionaTransizione("Seleziona la transizione da eseguire sulla macchina 2",reciprocamenteSincrone);
		
			// addato!!!
			if ( risultato[1]==null)
				risultato[0]=null;
					
			
		}else{//cioe' risultato[0] contiene una transizione asincrona o null
			
			Vector <Transizione> abilitate_2= getTransizioniAbilitate(1, SOLO_ASINCRONE);
			if(abilitate_2.size()==1)
				risultato[1]=abilitate_2.get(0);
			
			else if(abilitate_2.size()>1)
				risultato[1]=Input.selezionaTransizione("Seleziona la transizione da eseguire sulla macchina 2",abilitate_2);
			
		}
		
		/*Si considera il caso in cui ci siano transizioni in atto
		 * */
		for(int i=0; i<NUMERO_MACCHINE;i++)
			//System.out.println(transInAtto[1]);
			if(transInAtto[i]!=null)
				risultato[i]=transInAtto [i];
		
		 
		return risultato;
	}
	
	
	
	private Vector<Transizione> getReciprocamenteSincrone(TransizioneSincrona trans,int numeroMacchina){
		Vector <Transizione> reciprocamenteSincrone= new Vector<Transizione>();
		Transizione t;
		for(int i=0; i<transAttive[numeroMacchina].size(); i++){
			t=transAttive[numeroMacchina].get(i);
			if(t.getClass()==TransizioneSincrona.class)
				if(((TransizioneSincrona)t).getClasseEq().equals(trans.getClasseEq()))//se sono reciprocamente sincrone
						reciprocamenteSincrone.add((TransizioneSincrona)t);
		}//for
		return reciprocamenteSincrone;
		
	}
	
	/*@requires \forall int i; transDaEseguire[i]; i<NUMERO_MACCHINE;
	 @*/
	private int getDurataIterazione(Transizione[] transDaEseguire){
		if(transDaEseguire[0]==null &&transDaEseguire[1]==null)
			return 0;
		else if(transDaEseguire[0]==null)
			return transDaEseguire[1].getDurataresidua();
		else if(transDaEseguire[1]==null)
			return transDaEseguire[0].getDurataresidua(); 
		else
			return Math.min(transDaEseguire[0].getDurataresidua(), transDaEseguire[1].getDurataresidua());
		
	}
	
	/*@requires numeroMacchina<= NUMERO_MACCHINE && t != null &&durataIterazione>=0;
	  @ensure  "se non sono rimaste transizioni in atto" transInAtto = null && transEffettuata != null
	  @@ensure  "se e' stata effetuata una transizione" transInAtto != null && transEffettuata = null
	 @*/
	private void eseguiTransizione(Transizione t, int numeroMacchina, int durataIterazione){
		
		if(durataIterazione>=t.getDurataresidua()){
			fsm[numeroMacchina].setStatoCorrente(t.getDestinazione());
			t.setDurataresidua(t.getDurata());
			transInAtto[numeroMacchina]=null;
			transEffettuata[numeroMacchina]=t;
			
		}
		else{
			t.setDurataresidua(t.getDurata()-durataIterazione);
			transInAtto[numeroMacchina]=t;
			transEffettuata[numeroMacchina]=null;
		}
	}
	
		
	
	public Vector<Transizione>[] getTransAttive() {
		return transAttive;
	}

	public void setTransAttive() {
		for(int i=0;i<NUMERO_MACCHINE;i++)
			transAttive[i]=fsm[i].getTransizioniAttive();//prova una stampa delle transizioni attive
	}

	public Macchina[] getFsm() {
		return fsm;
	}

	public void setFsm(Macchina[] fsm) {
		this.fsm = fsm;
	}

	public int getIstanteCorrente() {
		return istanteCorrente;
	}

	public void setIstanteCorrente(int istanteCorrente) {
		this.istanteCorrente = istanteCorrente;
	}

	
	public Transizione[] getTransEffettuata() {
		return transEffettuata;
	}

	public void setTransEffettuata(Transizione[] transEffettuata) {
		this.transEffettuata = transEffettuata;
	}

	public Transizione[] getTransInAtto() {
		return transInAtto;
	}

	public void setTransInAtto(Transizione[] transInAtto) {
		this.transInAtto = transInAtto;
	}
	
	
	
	
}
